1. Field of the Present Invention
The present invention relates to the field of logic design verification and more particularly to a method for extending the verification coverage achieved with traditional non-formal verification techniques such as simulation.
2. History of Related Art
Verification of digital hardware is generally accomplished by a simulation technique in which a given set of input test vectors is applied to a model of the circuit to be verified. Traditional simulation, however, is significantly limited in its ability to completely verify complex hardware. The number of states, state transitions, and state transition sequences associated with any particular digital circuit all increase exponentially as the model size, calculated in terms of the number of latches comprising the model, increases linearly. Referring to FIG. 1, a state transition diagram 100 representing various states and transition paths between the various states for a given logic design is presented where a transition path is defined as a sequence of one or more transitions and a transition is defined as a single step from a present state to a next state under control of the present input. State transition diagram 100 includes an initial state 102a and multiple transition paths 104a, 104b, and 104c, leading from initial transition state 102a to next transition states 102b, 102c, and 102d. Each of the states 102b, 102c, and 102d can transition to other states indicated in transition table 100 through the various transition paths. It will be appreciated by those skilled in the field of digital hardware design that state transition diagram 100 of FIG. 1 is a grossly simplified representation of the state machines contemplated by complex digital circuitry. It will be further appreciated that the number of transition states 102 and, correspondingly, the number of transition paths 104 increases exponentially with the number of latches, such that even a moderately complex circuit comprised of, for example, 1000 latches can assume 21000 or roughly 10300 states. Traditionally, conventional simulation techniques verify a given digital circuit in a depth-first fashion. As an example, a simulation technique might attempt to verify the digital circuit represented by state diagram 100 by applying a sequence of inputs to a model of the digital circuit and recording the transition paths that the model follows. Thus, for example, a given simulation trace may follow the digital circuit from an initial state 102a through intermediate states 102c and 102e to a final state 102f via transition paths 104b, 104d and 104e. If any rules or specifications with which the digital circuit must comply are violated along the transition path indicated from initial state 102a to final state 102f, the simulation trace indicated will identify the violation. As the number of states and transition paths increases exponentially with the number of latches in the circuit, achieving any significant coverage of the total number of available transition paths quickly becomes exceedingly difficult using conventional simulation techniques because each simulation run exposes only a single transition path. Circuit simulation is commonly referred to as a non-formal verification technique to emphasize the limited coverage achieved using such a technique. At the other end of the verification spectrum, formal verification tools and techniques are used to rigorously verify that an implantation satisfies a given specification or set of rules. Typically, a formal verification technique utilizes a breadth-first approach in which each possible transition path from a given transition state is verified before proceeding to another state (or set of states) in the machine. In the depiction of FIG. 1, for example, a formal verification technique might begin by verifying transition paths 104a, 104b, and 104c with respect to state 102a before proceeding to the second xe2x80x9ctierxe2x80x9d of states including states 102b, 102c, and 102d. After verifying each transition path 104 leading from the second tier of states, a formal verification tool might verify each transition path extending from the second tier of states to the third tier, and so forth. In this manner, a formal verification technique verifies essentially every permitted combination of transitions in state diagram 100. While formal verification tools and techniques obviously enjoy the advantage of the greatest possible coverage of the digital circuit being verified, it will be readily appreciated that the computational load contemplated by a full formal verification of a digital circuit with any significant complexity can quickly become overwhelming. Typically, therefore, formal verification tools are utilized in conjunction with an environment that is associated with the design to be verified. A model, such as an HDL model is imported into a formal verification tool such as a model checker. A verification engineer then constructs an environment around the design consisting of a variety of input constraints associated with the circuit. In addition, a set of properties or rules to be verified is supplied to the formal verification tool. The verification tool will then extract the full state transition table for the design limited by the environmental constraints. While this type of formal verification provides the desirable level of verification coverage, the construction of the environment around the design is a manually intensive, arduous, and time consuming process. It is therefore highly desirable to implement a verification technique striking a reasonable compromise between the limited coverage afforded by conventional simulation techniques and the expense and time consumed by formal verification methods.
The problems identified above are in large part addressed by a verification method according to the present invention in which a conventional non-formal verification tool is utilized to generate information from which a partial state transition diagram of the circuit to be verified can be extracted. A formal verification tool such as a model checker is then used to achieve formal verification of the portion of the circuit represented by the extracted state transition information. By combining non-formal with formal verification techniques, the invention is able to achieve additional verification coverage over the coverage provided by traditional simulation with only an incremental increase in the amount of time and expense required to generate the simulation.
Broadly speaking, the present invention contemplates the use of a two stage verification process in which the second stage augments verification coverage obtained by the first stage in an automatic fashion. In the first stage, state transition information is extracted from the output of a non-formal verification technique. A formal verification tool is then applied to the extracted state transition information to extend the verification coverage of the digital circuit beyond the coverage that is achieved using the first verification technique. In one embodiment, the method includes the initial step of applying a first verification technique such as a simulation technique to a model of the digital circuit. In one embodiment, the information from which the state transition information is extracted includes an all events trace that is produced by executing a set or plurality of simulation runs using the simulation tool or technique. In the preferred embodiment, the application of the formal verification tool comprises applying a model checker to the extracted state transition data to achieve a formal verification of the state machine represented by the state transition diagram. In one embodiment, the extracted state transition information includes a set of data points each representing a present state, a present input, and a next state. Preferably, the state transition information is sorted by the present state information to facilitate a breadth-first verification by the formal verification tool. In one embodiment useful for extending the verification coverage provided by a conventional non-formal verification technique, the non-formal tool is used to verify satisfaction of a specification or rule by traversing a first transition path of the circuit. The non-formal tool is then used a second time to verify the rule or specification by traversing a second transition path. State transition information generated during the first and second passes of the non-formal verification technique is then extracted and provided to a formal verification tool such as a model checker. The formal verification of the circuit represented by the extracted state transition information extends the verification coverage achieved with the non-formal verification tool such as by, for example, traversing the digital circuit with a third transition path that was not explored with the non-formal verification tool. In addition, infinite loop conditions or live lock conditions may be detected by applying the formal verification technique to the extracted state transition information. The invention further contemplates a computer system and a computer program product such as a computer readable medium for implementing the method of verifying digital circuits described herein.